ds:x:Id fp Type, da:k:Knd fp Type, upd:update-spec(ds;da). update-spec-vars(upd)  Id List 

latex

Definitions	update-spec(ds;da), update-spec-vars(upd), map(f;as), fpf-domain(f), type List, , State(ds), Valtype(da;k), 1of(t), x:AB(x), f(x)?z, IdDeq, 2of(t), x.A(x), Void, x:AB(x), Knd, a:A fp B(a), x:A. B(x), x. t(x), Type, t  T, Id, Top
Lemmas	fpf-domain wf, fpf-trivial-subtype-top, map wf, Id wf, fpf wf, Knd wf, pi2 wf, id-deq wf, fpf-cap wf, pi1 wf, ma-valtype wf, decl-state wf, nat wf